{-# OPTIONS -fglasgow-exts #-}

-----------------------------------------------------------------------------
-- |
-- Maintainer  :  joost.visser@di.uminho.pt, alcino@di.uminho.pt
-- Stability   :  experimental
-- Portability :  portable
--
-- Point-free rewrite rules
--
-----------------------------------------------------------------------------

module Data.Transform.RulesPF where

import Data.Transform.Type hiding ((/\))
import Data.Transform.Rewriting
import Control.Monad
import Debug.Trace


infixr 5 /\
(/\) ::  PF (a -> b) -> PF (a -> c) -> PF (a -> (b,c))
(/\) = SPLIT

-- Predicates for point-free rewriting

projected :: Query Bool
projected (PF t :| x) = (everything (||) aux (PF t :| reduce compr t x))
    where aux :: GenericQ Bool
          aux (PF _) (COMP _ FST HOLE) = True
          aux (PF _) (COMP _ SND HOLE) = True
          aux (PF _) (COMP _ FST (COMP _ HOLE _)) = True
          aux (PF _) (COMP _ SND (COMP _ HOLE _)) = True
          aux _ _ = False

injected :: Query Bool
injected (PF t :| x) = (everything (||) aux (PF t :| reduce compl t x))
    where aux :: GenericQ Bool
          aux (PF _) (COMP _ HOLE INL) = True
          aux (PF _) (COMP _ HOLE INR) = True
          aux (PF _) (COMP _ (COMP _ _ HOLE) INL) = True
          aux (PF _) (COMP _ (COMP _ _ HOLE) INR) = True
          aux _ _ = False

applied :: Query Bool
applied (PF t :| x) = (everything (||) aux (PF t :| reduce compr t x))
    where aux :: GenericQ Bool
          aux (PF _) (COMP _ AP (SPLIT HOLE _)) = True
          aux (PF _) (COMP _ AP (SPLIT (COMP _ HOLE _) _)) = True
          aux _ _ = False

-- Rules for point-free rewriting

comp_assocr :: Rule
comp_assocr _ (COMP a (COMP b f g) h) = return (COMP b f (COMP a g h))
comp_assocr _ _ = fail "Cannot apply Comp-Assoc!"

comp_assocl :: Rule
comp_assocl _ (COMP a f (COMP b g h)) = return (COMP b (COMP a f g) h)
comp_assocl _ _ = fail "Cannot apply Comp-Assoc!"

nat_id :: Rule
nat_id _ (COMP _ ID f) = return f
nat_id _ (COMP _ f ID) = return f
nat_id _ _ = fail "Cannot apply Nat_Id!"

bang_eta :: Rule
bang_eta _ BANG = mzero
bang_eta (Func _ One) _ = return BANG
bang_eta _ _ = mzero

eta_prod :: Rule
eta_prod _ (SPLIT _ _) = fail "Cannot apply Eta_Prod to Split!"
eta_prod (Func (Either _ _) (Prod _ _)) _ = fail "Priority to Sums!"
eta_prod (Func _ a@(Prod _ _)) f = 
    do c <- context
       guard (not (projected c))
       success "Eta-Prod" ((COMP a FST f) /\ (COMP a SND f))
eta_prod _ _ = fail "Cannot apply Eta_Prod!"

prod_cancel :: Rule
prod_cancel _ (COMP _ FST (SPLIT f g)) = success "Prod-Cancel" f
prod_cancel _ (COMP _ SND (SPLIT f g)) = success "Prod-Cancel" g
prod_cancel _ (COMP _ FST (COMP a (SPLIT f g) h)) = success "Prod-Cancel" (COMP a f h)
prod_cancel _ (COMP _ SND (COMP a (SPLIT f g) h)) = success "Prod-Cancel" (COMP a g h)
prod_cancel _ _ = fail "Cannot apply Prod_Cancel!"

prod_reflex :: Rule
prod_reflex _ (SPLIT FST SND) = success "Prod-Reflex" ID
prod_reflex _ _ = fail "Cannot apply Prod_Reflex!"

prod_fusion :: Rule
prod_fusion _ (COMP a (SPLIT f g) h) = success "Prod-Fusion" ((COMP a f h) /\ (COMP a g h))
prod_fusion _ _ = fail "Cannot apply Prod_Fusion!"

prod_eta :: Rule
prod_eta a (SPLIT (COMP b FST f) (COMP c SND g)) =
    do Eq <- teq b c
       guard (geq (PF a) f g)
       success "Prod-Eta" f
prod_eta _ _ = fail "Cannot apply Eta-Prod!"

prod_def :: Rule
prod_def (Func (Prod a b) _) (PROD f g) = success "Prod-Def" ((COMP a f FST) /\ (COMP b g SND))
prod_def _ _ = fail "Cannot apply Prod-Def!"

{-
prod_fusion' :: Rule
prod_fusion' _ (COMP (Prod a b) (PROD f g) (PROD h k)) = success "Prod-fusion'" 
                                                             (PROD (COMP a f h) (COMP b g k))
prod_fusion' _ (COMP (Prod a b) (PROD f g) (COMP t (PROD h k) j)) = success "Prod-fusion'" 
                                                       (COMP t (PROD (COMP a f h) (COMP b g k)) j)
prod_fusion' _ _ = fail "Cannot apply Prod-fusion'!" 
-}

prod_id :: Rule
prod_id _ (PROD ID ID) = return ID
prod_id _ _            = fail "Cannot apply Prod-Id"

prod_elim :: Rule
prod_elim (Func (Prod a _) _) (COMP _ FST (PROD f _)) = success "Prod-Elim" $ COMP a f FST
prod_elim (Func (Prod _ b) _) (COMP _ SND (PROD _ g)) = success "Prod-Elim" $ COMP b g SND
prod_elim _ _ = fail "Cannot apply Prod-Elim!"

prod_elim' :: Rule
prod_elim' _ (COMP _ FST (COMP (Prod a b) (PROD f _) x)) = 
                                        success "Prod-Elim'" $ COMP a f (COMP (Prod a b) FST x)
prod_elim' _ (COMP _ SND (COMP (Prod a b) (PROD _ g) x)) = 
                                        success "Prod-Elim'" $ COMP b g (COMP (Prod a b) SND x)
prod_elim' _ _ = fail "Cannot apply Prod-Elim'!"


split_fusion :: Rule
split_fusion _ (COMP (Prod t1 t2) (PROD a b) (SPLIT c d))
   = success "Split-Fusion'" $ SPLIT (COMP t1 a c) (COMP t2 b d)
split_fusion _ _ = fail "Cannot apply Split-Fusion!"

mapjoin1_elim :: Rule
mapjoin1_elim _ (COMP (Map a _) DOM MapJoin1)
   = success "MapJoin1-Elim" $ COMP (Map a One) DOM FST
mapjoin1_elim _ _ = fail "Cannot apply MapJoin1-Elim"

mapjoin2_elim :: Rule
mapjoin2_elim _ (COMP (Map a (Prod b _)) DOM MapJoin2)
   = success "MapJoin2-Elim" $ COMP (Map a b) DOM FST
mapjoin2_elim _ _ = fail "Cannot apply MapJoin2-Elim"

coUnMapsum1_elim :: Rule
coUnMapsum1_elim _ (COMP (Map a _) DOM RCoUnMapsum1)
   = success "CoUnMapsum1-Elim" $ COMP (Map a One) DOM FST
coUnMapsum1_elim _ _ = fail "Cannot apply CoUnMapsum1-Elim"

coUnMapsum2_elim :: Rule
coUnMapsum2_elim _ (COMP (Map a (Prod b _)) DOM RCoUnMapsum2)
   = success "CoUnMapsum2-Elim" $ COMP (Map a b) DOM FST
coUnMapsum2_elim _ _ = fail "Cannot apply CoUnMapsum2-Elim"


eta_sum :: Rule
eta_sum _ (EITHER _ _) = fail "Cannot apply Eta_Sum to Either!"
eta_sum (Func a@(Either _ _) _) f = 
    do c <- context
       guard (not (injected c))
       success "Eta-Sum" (EITHER (COMP a f INL) (COMP a f INR))
eta_sum _ _ = fail "Cannot apply Eta-Sum!"

sum_cancel :: Rule
sum_cancel _ (COMP _ (EITHER f g) INL) = success "Sum-Cancel" f
sum_cancel _ (COMP _ (EITHER f g) INR) = success "Sum-Cancel" g
sum_cancel _ (COMP _ (COMP a h (EITHER f g)) INL) = success "Sum-Cancel" (COMP a h f)
sum_cancel _ (COMP _ (COMP a h (EITHER f g)) INR) = success "Sum-Cancel" (COMP a h g)
sum_cancel _ _ = fail "Cannot apply Sum-Cancel!"

sum_def :: Rule
sum_def (Func _ (Either a b)) (SUM f g) = success "Sum-Def" (EITHER (COMP a INL f) (COMP b INR g))
sum_def _ _ = fail "Cannot apply Sum-Def!"

eta_exp :: Rule
eta_exp _ (CURRY _) = fail "Cannot apply Eta-Exp to Curry!"
eta_exp (Func a (Func b c)) f =
    do x <- context
       guard (not (applied x))
       success "Eta-Exp" (CURRY (COMP (Prod (Func b c) b) AP (COMP a f FST /\ SND)))
eta_exp _ _ = fail "Cannot apply Eta-Exp!"


exp_cancel :: Rule
exp_cancel (Func a _) (COMP (Prod _ b) AP (SPLIT (CURRY f) h)) = success "Exp-Cancel" (COMP (Prod a b) f (ID /\ h))
exp_cancel _ (COMP (Prod _ b) AP (SPLIT (COMP a (CURRY f) g) h)) = success "Exp-Cancel" (COMP (Prod a b) f (g /\ h))
exp_cancel _ _ = fail "Cannot apply Exp-Cancel!"

exp_def :: Rule
exp_def (Func (Func _ a) _) (EXP f) = success "Exp-Def" (CURRY (COMP a f AP))
exp_def _ _ = fail "Cannot apply Exp-Def!"

listmap_fusion :: Rule
listmap_fusion _ (COMP (List t) (LIST f) (LIST g)) = success "Listmap-Fusion_1" (LIST (COMP t f g))
listmap_fusion _ (COMP (List t) (LIST f) (COMP t' (LIST g) h)) = success "Listmap-Fusion_1" (COMP t' (LIST (COMP t f g)) h)
listmap_fusion _ _ =  fail "Cannot apply Listmap-Fusion"

listmap_id :: Rule
listmap_id _ (LIST ID) = return ID
listmap_id _ _ = fail "Cannot apply Listmap-Id"

setmap_id :: Rule
setmap_id _ (SET ID) = return ID
setmap_id _ _        = fail "Cannot apply Setmap-Id"

maybe_id :: Rule
maybe_id _ (MAYBE ID) = return ID
maybe_id _ _          = fail "Cannot apply Maybe-Id"

mapkeys_id :: Rule
mapkeys_id _ (MAPKEYS ID) = return ID
mapkeys_id _ _            = fail "Cannot apply Mapkeys-Id"

either_id :: Rule
either_id _ (SUM ID ID) = return ID
either_id _ _           = fail "Cannot apply Either-Id"

comp_id :: Rule
comp_id _ (COMP _ ID x) = return x
comp_id _ (COMP _ x ID) = return x
comp_id _ _           = fail "Cannot apply Comp-Id"

mapkeys_fusion :: Rule
mapkeys_fusion (Func (Map a _) _) (COMP _ DOM (MAPKEYS f))
   = success "Mapkeys-Fusion" $ COMP (Set a) (SET f) DOM
mapkeys_fusion _ (COMP _ RNG (MAPKEYS _))
   = success "Mapkeys-Fusion" $ RNG
mapkeys_fusion _ _ = fail "Cannot apply Mapkeys-Fusion"

map_fusion :: Rule
map_fusion _ (COMP _ DOM (MAP _))
   = success "Map-Fusion" DOM
map_fusion (Func (Map _ c) _) (COMP _ (RNG) (MAP f))
   = success "Map-Fusion" $ COMP (Set c) (SET f) RNG
map_fusion _ _ = fail "Cannot apply Map-Fusion"

split_simpl :: Rule
split_simpl _ (SPLIT (COMP t1 f FST) (COMP t2 g FST)) = do
   Eq <- teq t1 t2
   success "Split-Simpl" $ COMP t1 (SPLIT f g) FST
split_simpl _ (SPLIT (COMP t1 f SND) (COMP t2 g SND)) = do
   Eq <- teq t1 t2
   success "Split-Simpl" $ COMP t1 (SPLIT f g) SND
split_simpl _ _ = fail "Cannot apply Split-Simpl"

mapmap_fusion :: Rule
mapmap_fusion _ (COMP (Map k v) (MAP f) (COMP t (MAP g) h)) = success "Mapmap-Fusion" (COMP t (MAP (COMP v f g)) h)
mapmap_fusion _ (COMP (Map k v) (MAP f) (MAP g)) = success "Mapmap-Fusion" (MAP (COMP v f g))
mapmap_fusion _ _ =  fail "Cannot apply Mapmap-Fusion"

elems_fusion :: Rule
elems_fusion (Func (Map a b) (List c)) (COMP _ (LIST f) ELEMS) = success "Elems-Fusion" (COMP (Map a c) ELEMS (MAP f))
elems_fusion (Func _ (List c)) (COMP _ (LIST f) (COMP (Map a b) ELEMS h)) = success "Elems-Fusion" (COMP (Map a b) (COMP (Map a c) ELEMS (MAP f)) h)
elems_fusion _ _ = fail "Cannot apply Elems-Fusion"

elems_linv :: Rule
elems_linv _ (COMP _ ELEMS LIST2MAP)  = success "Elems-Linv" ID
elems_linv _ (COMP _ ELEMS (COMP _ LIST2MAP f)) = success "Elems-Linv" f
elems_linv _ _ = mzero

list2map_fusion :: Rule
list2map_fusion (Func _ (Map _ a)) (COMP _ (MAP f) LIST2MAP) = success "List2map-Fusion" (COMP (List a) LIST2MAP (LIST f))
list2map_fusion (Func _ (Map _ a)) (COMP _ (MAP f) (COMP b LIST2MAP g)) = success "List2map-Fusion" (COMP b (COMP (List a) LIST2MAP (LIST f)) g)
list2map_fusion _ _ = mzero

mapjoin_fusion :: Rule
mapjoin_fusion (Func _ (Map _ e)) (COMP (Map a (Prod b c)) (MAP f) (COMP _ LJOIN g)) = 
    do (COMP _ h FST) <- return $ reduce compl (Func (Prod b c) e) (COMP e ID f)
       success "Mapjoin-Fusion" (COMP (Prod (Map a b) (Func a c)) (COMP (Map a b) (MAP h) FST) g)
mapjoin_fusion _ _ = mzero



mapmap_id :: Rule
mapmap_id _ (MAP ID) = return ID
mapmap_id _ _ = fail "Cannot apply Mapmap-Id"

comp_distr :: Rule
comp_distr _ (COMP (Set t) (SET f) (SET g)) 
   = success "Comp-Distr" $ SET (COMP t f g)
comp_distr _ (COMP (List t) (LIST f) (LIST g))
   = success "Comp-Distr" $ LIST (COMP t f g)
comp_distr _ (COMP (Maybe t) (MAYBE f) (MAYBE g))
   = success "Comp-Distr" $ MAYBE (COMP t f g)
comp_distr _ (COMP (Map t _) (MAPKEYS f) (MAPKEYS g))
   = success "Comp-Distr" $ MAPKEYS (COMP t f g)
comp_distr _ (COMP (Map _ t) (MAP f) (MAP g))
   = success "Comp-Distr" $ MAP (COMP t f g)
comp_distr _ (COMP (Either t1 t2) (SUM f1 g1) (SUM f2 g2))
   = success "Comp-Distr" $ SUM (COMP t1 f1 f2) (COMP t2 g1 g2)
comp_distr _ (COMP (Prod t1 t2) (PROD f1 g1) (PROD f2 g2))
   = success "Comp-Distr" $ PROD (COMP t1 f1 f2) (COMP t2 g1 g2)
comp_distr _ (COMP t1 (SetInc t2 f g) h)
   = success "Comp-Distr" $ SetInc t2 (COMP t1 f h) (COMP t1 g h)
comp_distr _ (COMP t (AND p1 p2) x)
   = success "Comp-Distr" $ AND (COMP t p1 x) (COMP t p2 x)
comp_distr _ _ = fail "Cannot apply Comp-Distr!"

removeTags :: Rule
removeTags _ (COMP t f g) = return (COMP (rmTags t) f g)
removeTags _ x = return x

hardcore_elim :: Rule
hardcore_elim _ (COMP (Map a (Map b c)) (COMP _ (COMP _ SETFUSE (SET DOM)) RNG) MapJoin1)
   = success "Hardcore-Elim" $ COMP (Map (Prod a b) c) (COMP (Set (Prod a b)) (SET SND) DOM) SND
hardcore_elim _ _ = fail "Cannot apply Hardcore-Elim!"





-- | Simplify relational rules
--   imported form 2lt-inv
--
simplifyRel :: Rule
simplifyRel = normalizeAnd >>> (simplifyAnd ||| simplifyInv)


-- | Normalize Ands
normalizeAnd :: Rule
normalizeAnd  = many (once assocAndToRight)


-- | Associate And expressions to the right
assocAndToRight :: Rule
assocAndToRight _ (COMP t (AND r1 r2) r3) = return $ AND (COMP t r1 r3) (COMP t r2 r3)
assocAndToRight _ (AND (AND a b) c) = return $ AND a (AND b c)
assocAndToRight _ _ = mzero


-- | Simplify nested And predicate functions
--   This function assumes that ands are nested to right
simplifyAnd :: Rule
simplifyAnd t (AND x a@(AND _ _))
   = do x' <- simplifyInv t x
        a' <- simplifyAnd t a
        return $ AND x' a'
simplifyAnd t (AND x y)
   = do x' <- simplifyInv t x
        y' <- simplifyInv t y
        return $ AND x' y'
simplifyAnd _ _ = mzero


simplifyInv :: Rule
simplifyInv = many (enable allRules)

  
-- | Enable a rule by associating terms to right in top-down order and then
--   associating them to left in bottom-up. 
enable :: Rule -> Rule
enable r t x = (r t x) 
            `mplus` 
             (do x' <- once (top comp_assocr) t x
                 enable r t x') 
            `mplus` 
             (enablel r t x)
   where enablel r t x = (r t x) 
                      `mplus` 
                       (do x' <- onceBU (top comp_assocl) t x -- is this onceBU ok? seems
                           enablel r t x')


allRules :: Rule
allRules = once (aux1 ||| aux2 ||| aux3 ||| aux4 )
  where
    aux1 = top nat_id ||| top prod_cancel ||| top prod_eta ||| 
	         top prod_reflex ||| top prod_fusion -- ||| top prod_def

    aux2 = top nat_id ||| top sum_cancel ||| top sum_def

    aux3 = top listmap_id ||| top listmap_fusion ||| top mapmap_fusion ||| 
           top elems_fusion ||| top mapjoin_fusion ||| top list2map_fusion ||| 
           top mapmap_id ||| top elems_linv ||| top bang_eta 

    aux4 = {-top eta_prod ||| -}top prod_id ||| top prod_elim ||| top split_fusion ||| 
           top mapjoin1_elim ||| top mapjoin2_elim ||| top coUnMapsum1_elim |||
           top coUnMapsum2_elim ||| top eta_sum ||| top eta_exp ||| top exp_cancel |||
           top exp_def ||| top setmap_id ||| top maybe_id ||| top mapkeys_id |||
           top either_id ||| top comp_id ||| top mapkeys_fusion ||| top map_fusion |||
           top split_simpl ||| top comp_distr ||| top hardcore_elim

  --  aux5 = top map2mapsElim



-- some rules to the rdb 2 ss
{-
map2mapsElim :: Rule
map2mapsElim _ (COMP _ DOM (COMP _ FST Map2maps)) = success "Map2mapsElim" DOM
map2mapsElim _ (COMP _ DOM (COMP _ FST (COMP x Map2maps g))) = 
                                                  success "Map2mapsElim" (COMP x DOM g)
map2mapsElim _ (COMP _ DOM (COMP _ SND Map2maps)) = success "Map2mapsElim" DOM
map2mapsElim _ (COMP _ DOM (COMP _ SND (COMP x Map2maps g))) = 
                                                  success "Map2mapsElim" (COMP x DOM g)
map2mapsElim _ _ = fail "Cannot apply Map2mapsElim!"


-- [(A * B) * C] -> Map (A * B) C -> Set (A * B) -> Set A
-- (set fst) . (dom . table2map) 
-- == list2set . (map fst.fst)
-- [(A * B) * C] -> [A] -> Set A
-- 
table2mapElim :: Rule
table2mapElim _ (COMP (Set (Prod a b)) (SET FST) (COMP _ DOM Table2map)) = success "Table2mapElim" 
                                 (COMP (List a) LIST2SET (LIST (COMP (Prod a b) FST FST)))
table2mapElim _ (COMP (Set (Prod a b)) (SET FST) (COMP _ DOM (COMP x Table2map f))) = success 
          "Table2mapElim" (COMP (List a) LIST2SET (COMP x (LIST (COMP (Prod a b) FST FST)) f))
table2mapElim _ _ = fail "Cannot apply Table2mapElim"
-}

simplifyrdb :: Rule
simplifyrdb = many (prodsrdb ||| mapsrdb ||| others) >>> compr


{-
myRules :: Rule
myRules = many1 (compr >>> once aux)
  where
    aux =  top map2mapsElim ||| top table2mapElim
-}

prodsrdb :: Rule
prodsrdb = many1 (compr >>> once aux)
  where 
	  aux =  top prod_elim  |||
           top prod_elim' |||  top nat_id ||| top prod_eta ||| top prod_cancel |||  
           top prod_reflex |||
           top prod_fusion  ||| top prod_def ||| top prod_id ||| top comp_distr

mapsrdb :: Rule
mapsrdb = many1 (compr >>> once aux)
   where
     aux = top listmap_id ||| top listmap_fusion ||| top mapmap_fusion ||| 
           top elems_fusion ||| top mapjoin_fusion ||| top list2map_fusion ||| 
           top mapmap_id ||| top elems_linv ||| top bang_eta

others :: Rule
others = many1 (compr >>> once aux)
  where
    aux =  top split_fusion ||| 
           top mapjoin1_elim ||| top mapjoin2_elim ||| top coUnMapsum1_elim |||
           top coUnMapsum2_elim ||| top eta_sum ||| top eta_exp ||| top exp_cancel |||
           top exp_def ||| top setmap_id ||| top maybe_id ||| top mapkeys_id |||
           top either_id ||| top comp_id ||| top mapkeys_fusion ||| top map_fusion |||
           top split_simpl ||| top hardcore_elim |||
           top nat_id ||| top prod_cancel ||| top prod_eta ||| 
	         top prod_reflex ||| top prod_fusion |||
           top nat_id ||| top sum_cancel ||| top sum_def |||
           top listmap_id ||| top listmap_fusion ||| top mapmap_fusion ||| 
           top elems_fusion ||| top mapjoin_fusion ||| top list2map_fusion ||| 
           top mapmap_id ||| top elems_linv ||| top bang_eta ||| 
           top prod_id ||| top prod_elim ||| top split_fusion ||| 
           top mapjoin1_elim ||| top mapjoin2_elim ||| top coUnMapsum1_elim |||
           top coUnMapsum2_elim ||| top eta_sum ||| top eta_exp ||| top exp_cancel |||
           top exp_def ||| top setmap_id ||| top maybe_id ||| top mapkeys_id |||
           top either_id ||| top comp_id ||| top mapkeys_fusion ||| top map_fusion |||
           top split_simpl ||| top comp_distr ||| top hardcore_elim 



-- Rewriting systems for point-free

optimize :: Rule
optimize = everywhere (top removeTags) >>> many (prods ||| maps ||| sums) >>> compr


rtrace :: Rule
rtrace t x = return (trace msg x)
  where
    msg = show (length str) -- ++"\n"++take 200 str
    str = gshow (PF t) x

-- | Associate all compositions to the right
compr :: Rule
compr = many (once (top comp_assocr))

-- | Associate all compositions to the left
compl :: Rule
compl = many (once (top comp_assocl))

prods :: Rule
prods = many1 (compr >>> once aux)
    where aux :: Rule
	  aux =  top nat_id ||| top prod_eta ||| top prod_cancel ||| 
	         top prod_reflex ||| top prod_fusion ||| top prod_def

sums :: Rule
sums = many1 (compl >>> once aux)
    where aux :: Rule
	  aux = top nat_id ||| top sum_cancel ||| top sum_def

maps :: Rule
maps = many1 (compr >>> once aux)
   where
     aux = top listmap_id ||| top listmap_fusion ||| top mapmap_fusion ||| top elems_fusion ||| top mapjoin_fusion ||| top list2map_fusion ||| top mapmap_id ||| top elems_linv ||| top bang_eta 

-- Example

assocr :: PF (((Int,Char),Bool) -> (Int,(Char,Bool)))
assocr = SPLIT (COMP typeof FST FST) (PROD SND ID)

assocl :: PF ((Int,(Char,Bool)) -> ((Int,Char),Bool))
assocl = SPLIT (PROD ID FST) (COMP typeof SND SND)

associso = simplify True prods (COMP typeof assocr assocl)

-- Complete systems

simplifyPF = reduceMaybe optimize
